Route (a): mechanise the impossibility. EchoThermoCollapseImpossible
proves the doc's own kill condition, second horn — (i)∧(ii) ⊢ ⊥ —
verbatim, for the obligation's named witness.

- nat-into-collapse-fiber{-injective}: ℕ ↪ Echo (const y₀) y₀ — the
  collapse fiber is infinite (the structural reason no finite count
  exists), recorded positively.
- collapse-cost-impossible: any total --safe cost on (ℕ → B) agreeing
  with fiber-erasure-bound on every finite restriction of the constant
  map is impossible — clause (ii) at n=1,2 (T=1, via FiberSize-fin-
  const, PR #58's honest count) forces its single value to be both 0
  and 1. Impossibility CONFIRMED.

The quantitative-collapse functional provably does not extend to an
infinite carrier as a total --safe function: a settled NEGATIVE
boundary, not an open gap, not a defect. Orthogonal to the Bennett
zero direction (closed for all carriers, this PR's earlier commit).

Governance docs flipped O-THERMO-∞ [OPEN] → [CLOSED-NEG] and the
Thermodynamic Direction [REAL*] → [REAL] (no open obligation remains);
STABILITY §3.3 re-rated B- → B / ~95% (standing B- freeze lifts —
discharged negatively counts as discharged; not higher since a
confirmed-negative is an honest limit, and the separate
Information-Theory Direction stays unbuilt).

All --safe --without-K, zero postulates, zero escape pragmas (the lone
'postulate' string is the comment false-positive class, EchoKernel
precedent). Smoke.agda + All.agda exit 0; new headlines pinned.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…nite)

Steps 1-3 of the thermodynamic-bridge continuation, stacked on PR #58.

1. EchoThermodynamicsArbitrary: FiberSubsingleton (K-free, --without-K
   safe surrogate for fibre isProp) + injective⇒fiber-subsingleton for
   an arbitrary carrier A : Set a (no Fin, no FiniteDomain).
2. reversible-erasure-cost (occupancy-keyed) + bennett-reversible-
   arbitrary: Bennett zero-cost for every injective map on any carrier,
   no finiteness. Anti-vacuity: occupancy≡FiberSize-fin and
   bennett-arbitrary-refines-finite certify the structural cost
   coincides with PR #58's established count and strictly subsumes it.
3. cno-identity over the genuine infinite absolute-zero Program carrier;
   bennett-reversible-cno-identity makes 'a CNO dissipates zero Landauer
   energy' a real theorem, not the historically vacuous claim.

EchoFiberCount: added FiberSize-fin-subsingleton (Headline 2c), the
finite-domain anti-vacuity hook (FiberSize-fin-injective is its
corollary; kept as-is upstream for pin stability).

O-THERMO-∞ unchanged and NOT discharged: re-narrowed in docs to be
specifically the quantitative-collapse functional on an infinite
carrier (orthogonal to the now-closed Bennett zero direction).

All --safe --without-K, zero postulates, zero escape pragmas.
Smoke.agda + All.agda exit 0. Docs (ECHO-CNO-BRIDGE §Thermodynamic
Bridge, STABILITY_ANALYSIS §3.3 ~90%/B-, MAP.adoc status tag) updated
in the same PR per the MAP governance rule.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Route (a): mechanise the impossibility. EchoThermoCollapseImpossible
proves the doc's own kill condition, second horn — (i)∧(ii) ⊢ ⊥ —
verbatim, for the obligation's named witness.

- nat-into-collapse-fiber{-injective}: ℕ ↪ Echo (const y₀) y₀ — the
  collapse fiber is infinite (the structural reason no finite count
  exists), recorded positively.
- collapse-cost-impossible: any total --safe cost on (ℕ → B) agreeing
  with fiber-erasure-bound on every finite restriction of the constant
  map is impossible — clause (ii) at n=1,2 (T=1, via FiberSize-fin-
  const, PR #58's honest count) forces its single value to be both 0
  and 1. Impossibility CONFIRMED.

The quantitative-collapse functional provably does not extend to an
infinite carrier as a total --safe function: a settled NEGATIVE
boundary, not an open gap, not a defect. Orthogonal to the Bennett
zero direction (closed for all carriers, this PR's earlier commit).

Governance docs flipped O-THERMO-∞ [OPEN] → [CLOSED-NEG] and the
Thermodynamic Direction [REAL*] → [REAL] (no open obligation remains);
STABILITY §3.3 re-rated B- → B / ~95% (standing B- freeze lifts —
discharged negatively counts as discharged; not higher since a
confirmed-negative is an honest limit, and the separate
Information-Theory Direction stays unbuilt).

All --safe --without-K, zero postulates, zero escape pragmas (the lone
'postulate' string is the comment false-positive class, EchoKernel
precedent). Smoke.agda + All.agda exit 0; new headlines pinned.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ive (#60)

Thermodynamic-bridge continuation. **Stacked on PR #58** (base =
`thermo/bennett-injective-finite-stack-2026-05-18`, itself on PR #54
`docs/echo-types-master-map`). Depends on #58's
`bennett-reversible-injective` / `FiberSize-fin-injective` /
`FiberSize-fin-const` and on MAP.adoc (only on the #54 branch).

**Re-target chain:** #54→main, then #58→main, then **this PR→main**.
(Automated poll armed; merges out-of-band.)

This PR closes the thermodynamic pillar: **no open obligation remains**
for the Thermodynamic Direction (`[REAL*]` → `[REAL]`, B- → B / ~95%).

## Part 1 — Bennett zero-cost on an arbitrary carrier (Steps 1–3)

The finiteness in PR #58 / `EchoThermodynamicsFinite` was an artefact of
routing cost through `FiberSize-fin` (an enumeration); Bennett's
physical content (no fan-in) needs no finiteness.

1. **`FiberSubsingleton` + `injective⇒fiber-subsingleton`** — K-free
`--without-K`-safe "no fan-in" predicate, for an **arbitrary** carrier
`A : Set a`. (Full fibre `isProp` would need `B` an h-set/UIP,
unavailable under `--without-K`; the first-projection form is what the
count needs.)
2. **`bennett-reversible-arbitrary`** — Bennett zero-cost for every
injective map on **any** carrier, no `Fin`/`FiniteDomain`, via an
occupancy-keyed `reversible-erasure-cost`. **Anti-vacuity:**
`occupancy≡FiberSize-fin` + `bennett-arbitrary-refines-finite` prove it
coincides with and strictly subsumes #58's established count.
3. **`bennett-reversible-cno-identity`** — instantiated at `cno-identity
: Program → Program` over the genuine **infinite** absolute-zero
`Program` carrier: "a CNO dissipates zero Landauer energy" is now a real
theorem, not the historically vacuous claim.

`EchoFiberCount` gains `FiberSize-fin-subsingleton`
(`FiberSize-fin-injective` is its corollary; kept as-is upstream for pin
stability).

## Part 2 — O-THERMO-∞ discharged negatively → `[CLOSED-NEG]`

Route (a): mechanise the impossibility. `EchoThermoCollapseImpossible`
proves the obligation's **own kill condition, second horn — (i)∧(ii) ⊢ ⊥
— verbatim**, for its named witness:

- `nat-into-collapse-fiber{-injective}`: `ℕ ↪ Echo (const y₀) y₀` — the
collapse fiber is infinite (the structural reason no finite count
exists).
- `collapse-cost-impossible`: any total `--safe` `cost` agreeing with
`fiber-erasure-bound` on every finite restriction of the constant map is
impossible — clause (ii) at `n = 1, 2` (`T = 1`, via
`FiberSize-fin-const`) forces its single value to be both `0` and `1`.

The quantitative-collapse functional provably does **not** extend to an
infinite carrier as a total `--safe` function: a settled negative
boundary, **not** a softened "future work" item and **not** a defect.
Orthogonal to the Bennett zero direction (closed for all carriers, Part
1).

## Verification

- All `--safe --without-K`, **zero postulates, zero escape pragmas**
(the lone `postulate` string is the comment false-positive class —
EchoKernel precedent).
- `Smoke.agda` + `All.agda` typecheck (exit 0); all new headlines pinned
in `Smoke.agda`.
- Governance docs updated same PR per the MAP rule:
`ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge" (O-THERMO-∞ →
`[CLOSED-NEG]`), `STABILITY_ANALYSIS.md` §3.3 (B / ~95%, with explicit
rationale for the freeze-lift), `docs/echo-types/MAP.adoc` (`[REAL*]` →
`[REAL]`, proofs list).

Honours retraction R-2026-05-18 — orthogonal; nothing retracted is
reinstated. The separate Information-Theory bridge (Theorem 5) remains
unbuilt by design — a different Direction.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

#57 reduced to its sole content not already in main: the new module
proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda (225 lines) +
Smoke pins + All.agda registration. F1/F4/F2 spikes and the doc
reframes from the original branch were superseded by #54/#55/#56/#58/#60
(present in main, byte-identical) and the Nix-flake commit dropped
(Guix-primary policy). Typechecks --safe --without-K, zero postulates;
full All.agda + Smoke + characteristic + examples suites green.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>